The geometric system of deduction called N-Graphs was introduced by de Oliveira in 2001. The proofs in this system are represented by means of digraphs and, while its derivations are mostly based on Gentzen's sequent calculus, the system gets its inspiration from geometrically based systems, such as the Kneales' tables of development, Statman's proofs-as-graphs, Buss' logical flow graphs, and Girard's proof-nets. Given that all these geometric systems appeal to the classical symmetry between premises and conclusions, providing an intuitionistic version of (...) any of these is an interesting exercise in extending the range of applicability of the geometric system in question. In this article we produce an intuitionistic version of N-Graphs, based on Maehara's LJ' system, as described by Takeuti. Recall that LJ' has multiple conclusions in all but the essential intuitionistic rules, e.g., implication right and negation right. We show soundness and completeness of our intuitionistic N-Graphs with respect to LJ'. We also discuss how we expect to extend this work to a version of N-Graphs corresponding to the intuitionistic logic system FIL (Full Intuitionistic Logic) of de Paiva and Pereira and sketch future developments. (shrink)

In an earlier study I argued that the appearance of the name of Memmius in the first, second, and fifth books alone of Lucretius de Rerum Natura is only the most striking indication of a fundamental change in the poet's attitude towards his reader which is already well established quite a short way through book 5, and which makes it almost incontestable that Lucretius wrote books 3, 4, and 6 after he had lost all hope of converting Memmius to Epicureanism.

Looking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to analyse the (...) role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory. (shrink)

The intention here is that of giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett–Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i.e. the so-called reduction rules. For that we suggest an extension (...) to the Curry– Howard interpretation which draws on the idea of labelled deduction, and brings back Frege’s device of variable-abstraction to operate on the labels (i.e., proof-terms) alongside formulas of predicate logic. (shrink)

Introduction to the concepts of Buddhist Abhidharma.

As a celebration of theTractatus100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that “everyone is aware of the holistic character of Wittgenstein’s later philosophy, but it is not so well known that it was already beginning to establish itself in theTractatus” (The False Prison, 1987). From the latter to the former, Stephen Hilmy’s (The Later Wittgenstein, 1987) extensive study of theNachlasshas helped removing classical misconceptions such as (...) Hintikka’s claim that “Wittgenstein in thePhilosophical Investigationsalmost completely gave up the calculus analogy.” Hilmy points out that even in theInvestigationsone finds the use of the calculus/game paradigm to the understanding of language, such as “in operating with the word” (Part I, §559) and “it plays a different part in the calculus”. Hilmy also quotes from a late (1946) unpublished manuscript (MS 130) “this sentence has use in the calculus of language”, which seems to be compatible with “asking whether and how a proposition can be verified is only a particular way of asking ‘How do you mean?’” Central in this back and forth there is an aspect which seems to deserve attention in the discussion of a semantics for the language of mathematics which might be based on (normalisation of) proofs and/or Hintikka/Lorenzen game-dialogue: the explication of consequences. Such a discussion is substantially supported by the use of the open and searchableThe Wittgenstein Archives at the University of Bergen. These findings are framed within the discussion of the meaning of logical constants in the context of natural deduction style rules of inference. (shrink)

The COVID-19 pandemic has forced developmental researchers to rethink their traditional research practices. The growing need to study infant development at a distance has shifted our research paradigm to online and digital monitoring of infants and families, using electronic devices, such as smartphones. In this practical guide, we introduce the Experience Sampling Method – a research method to collect data, in the moment, on multiple occasions over time – for examining infant development at a distance. ESM is highly suited for (...) assessing dynamic processes of infant development and family dynamics, such as parent-infant interactions and parenting practices. It can also be used to track highly fluctuating family dynamics and routines. The aim of the current paper was to provide an overview by explaining what ESM is and for what types of research ESM is best suited. Next, we provide a brief step-by-step guide on how to start and run an ESM study, including preregistration, development of a questionnaire, using wearables and other hardware, planning and design considerations, and examples of possible analysis techniques. Finally, we discuss common pitfalls of ESM research and how to avoid them. (shrink)